basic constructions:
strong axioms
further
In logic and foundations, a principle of omniscience is any principle of classical mathematics that is not valid in constructive mathematics. The idea behind the name (which is due to Bishop (1967)) is that, if we attempt to extend the computational interpretation of constructive mathematics to incorporate one of these principles, we would have to know something that we cannot compute. The main example is the law of excluded middle (); to apply computationally, we must know which of these disjuncts hold; to apply this in all situations, we would have to know everything (hence ‘omniscience’).
Bishop's principles of omniscience (stated below) may be seen as principles that extend classical logic from predicates (where may happen to be valid, even constructively, for certain predicates) to their quantifications over infinite domains (where is typically not constructively valid).
The limited principle of omniscience () states that the existential quantification of any decidable proposition is again decidable. That is,
or equivalently
We have not stated the domain of quantification of the variable . If you take it to be the subsingleton corresponding to a given truth value and apply this principle to the constantly true proposition, then follows; conversely, implies (over any domain). However, Bishop's takes the domain to be the set of natural numbers, giving a weaker principle than . (It appears that a realizability topos based on infinite-time Turing machines validates but not ; see Bauer (2011).) Note that propositions of the form when is decidable are the open truth values in the Rosolini dominance.
We can also state the principle set-theoretically, with explicit reference to the domain of quantification. Given a set , the limited principle of omniscience for () states that, given any function from to the boolean domain , either is the constant map to or belongs to the image of . Then Bishop's is , which applies to any infinite sequence of bits.
While for is a classic example of the difference between constructive and classical mathematics, holds for the set of extended natural numbers; this is related to the fact that may constructively be given a compact topology. See Escardó (2011) for this and much more.
The weak limited principle of omniscience () states that the universal quantification of any decidable proposition is again decidable. That is,
The lesser limited principle of omniscience () states that, if the existential quantification of the conjunction of two decidable propositions is false, then one of their separate existential quantifications is false. That is,
or equivalently
If, as before, you take the domains of quantification to be subsingletons, you get de Morgan's law (), which is weaker than ; conversely, implies (over any domain). Again, Bishop's takes the domain to be , giving a principle weaker than (and also weaker than ).
Stated set-theoretically, the lesser limited principle of omniscience for () states that, given functions , if , then or . So Bishop's is .
We have the following relations between the three principles of omniscience:
follows from , but not conversely. If is a decidable proposition, then so is , and so gives
which implies
as is decidable.
follows from , but not conversely.
In set theory, there are actually two different notions of logic: there is the external predicate logic used to define the set theory itself, and there is the internal predicate logic induced by the set operations on subsingletons and injections. In particular,
An internal proposition is a set such that for all elements and , .
The internal conjunction of two internal propositions and is the cartesian product of and .
The internal disjunction of two internal propositions and is the image of the unique function from the disjoint union of and to the singleton .
The internal implication of two internal propositions and is the function set between and .
The internal negation of an internal proposition is the function set from to the empty set
An internal proposition is a decidable proposition if it comes with a function from to the boolean domain .
An internal predicate on a set is a set with injection , whose family of propositions indexed by is represented by the preimages .
The internal existential quantifier of an internal predicate is the image of the unique function into the singleton .
Then the internal LPO for a family of sets is the LPO for each stated in the internal logic of the set theory:
or equivalently, as
Similarly, the internal WLPO for a family of sets is the WLPO for each stated in the internal logic of the set theory:
or equivalently
And finally, the internal LLPO for a family of sets is the LLPO for each stated in the internal logic of the set theory:
In particular, the internal LPO for the family of all subsingletons is internal excluded middle and the internal LLPO for the family of all subsingletons is internal weak excluded middle. Similarly, given a universe , the internal LPO for the family of all sets in is excluded middle in , and the internal LLPO for the family of all sets in is weak excluded middle in .
The internal versions of the principles of omniscience, like all internal versions of axioms, are weaker than the external version of the principle of omniscience, since while bounded separation implies that one can convert any external predicate on a set to an internal predicate , it is generally not possible to convert an internal predicate to an external predicate without a reflection rule which turns subsingletons in the set theory into propositions in the external logic.
In the context of dependent type theory, the various principles of omniscience can be translated in two ways, by interpreting “or” as propositionally truncated (“merely or”) or untruncated (“purely or”). The relationships between the truncated and untruncated principles of omniscience are as follows are:
Truncated LPO and untruncated LPO are equivalent (due to Martin Escardo, see UFP)
Similarly, truncated WLPO and untruncated WLPO are equivalent.
Untruncated LLPO is equivalent to WLPO (also due to Martin Escardo).
In http://www1.maths.leeds.ac.uk/~rathjen/Lifschitz.pdf is a model by Michael Rathjen that separates WLPO from LLPO. Similarly, Grossack 24 shows that Johnstone’s topological topos separates WLPO from LLPO.
Bishop introduced the above principles of omniscience to show that certain results in pointwise analysis could not be constructive, by showing that these results implied a principle of omniscience. There are similar axioms in analysis which imply the principles of omniscience for natural numbers, called analytic principles of omniscience, and include the following:
The analytic LPO states that the usual apartness relation on the set of real numbers is decidable ( or ), or equivalently trichotomy for the real numbers ( or or ), or equivalently, that the real numbers form a discrete field.
The analytic WLPO states that has decidable equality, or that the partial order on the real numbers is decidable ( or ).
The analytic LLPO states that the usual order on is a total order ( or ), which (by analogy with trichotomy) may be called dichotomy for the real numbers.
There are various other results that are equivalent to the principles of omniscience. Here are a few:
Let be the quotient of the unit interval that identifies the endpoints, and let be the quotient ring; both are classically isomorphic to the circle . (Constructively, we take to be , although can also be constructed as a completion of .) Constructively, there is an injection , which is a bijection if and only if the holds (for the appropriate kind of real number).
Every semi-decidable proposition is a decidable proposition iff holds.
Sequential compactness of the unit interval holds if and only if holds.
The boolean domain is a -frame if and only if holds, and it is the initial -frame if and only if holds.
The Cauchy real numbers are isomorphic to the radix expansion in any base (e.g., a decimal expansion or binary expansion) iff holds. See Feldman (2010).
Various analytic principles of omniscience are equivalent to the principles of omniscience for the natural numbers (see analytic principles of omniscience for proofs). More specifically:
The analytic LPO for the following sets of real numbers are equivalent to the LPO for the natural numbers: the Cauchy real numbers , the Escardo-Simpson real numbers/HoTT book real numbers /, and the subfield of Dedekind real numbers which are constructed out of Dedekind cuts valued in the initial -frame .
The analytic WLPO for the Cauchy real numbers is equivalent to the WLPO for the natural numbers.
The analytic LLPO for the Cauchy real numbers is equivalent to the LLPO for the natural numbers.
There are various other results that are related to the principles of omniscience. Here are a few:
In the presence of weak countable choice, there exists a radix expansion in any base (e.g., a decimal expansion or binary expansion) for every Cauchy real number iff holds. Without weak countable choice, Lifschitz realizability gives a model in which holds but it is not true that there exists a radix expansion in any base for every Cauchy real number. See Swan (2024).
In the presence of countable choice, is equivalent to the claim that the rings of radix expansions in any two bases are isomorphic. See Daniel Mehkeri's answer to Feldman (2010).
The full bar theorem implies the .
The existence of various classical universes or models of foundations of mathematics implies the :
Any model of bounded Zermelo set theory contains a pure set of real numbers . One can collect all the pure sets of which are in and show that the resulting set is a subset of and a sequentially Cauchy complete Archimedean ordered field which satisfies the analytic LPO, thus implying for the entire foundations. Thus, the existence of stronger models of material set theory such as ZFC also imply for the entire foundations.
For a similar reason, the existence of a constructively well-pointed Boolean W-topos implies the , since the hom-set , where is the terminal generator and is the real numbers object in , yields a sequentially Cauchy complete Archimedean ordered field which satisfies the analytic LPO, thus implying for the entire foundations. Thus, the existence of any constructive model of ETCS also implies for the entire foundations.
Finally, in dependent type theory, there being a univalent Tarski universe closed under dependent product types, dependent sum types, and identity types and satisfying the axiom of infinity and excluded middle implies the , since one can construct an element representing the -small type of real numbers, whose type reflection is a sequentially Cauchy complete Archimedean ordered field which satisfies the analytic LPO, thus implying for the entire type theory. Thus, any univalent Tarski universe which has axiom of choice or a choice operator for the types in the universe also implies for the entire type theory.
Note that in all these cases, the real numbers constructed from these universes or classical models of foundations of mathematics, while equivalent to the internal Dedekind real numbers constructed in the universe or model, are not necessarily equivalent to the external Dedekind real numbers in the foundations.
Assuming that Set is a Boolean topos, then (the LPO for natural numbers) holds in any presheaf topos over and indeed in any locally connected topos over , essentially since then is a constant object.
The LPO for natural numbers fails in Johnstone’s topological topos, due to its internal continuity principle. Hence, the analytic LPO also fails, since the modulated Cauchy reals and Dedekind reals coincide in this topos. However, the (analytic) LLPO holds, as a consequence of the preservation of finite closed unions by the inclusion of sequential spaces.
Errett Bishop: Foundations of Constructive Analysis, McGraw-Hill (1967)
(in the introduction or chapter 1, I forget)
Fred Richman, Polynomials and linear transformations. Linear Algebra and its Applications, Volume 131, 1 April 1990, Pages 131-137. [doi:10.1016/0024-3795(90)90379-Q]
Hajime Ishihara, Reverse Mathematics in Bishop’s Constructive Mathematics, Philosophia Scientiæ, CS 6 (2006) (doi:10.4000/philosophiascientiae.406, pdf)
David Feldman (2010) on Math.Overflow, Radix notation and toposes
Andrej Bauer (2011) via constructivenews, An Injection from to (pdf)
Martín Escardó (2011) via constructivenews, Infinite sets that satisfy the principle of omniscience in all varieties of constructive mathematics (pdf)
Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)
Michael Rathjen, Constructive Zermelo-Fraenkel set theory and the limited principle of omniscience. [arXiv:1302.3037]
Mike Shulman, Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, Mathematical Structures in Computer Science Vol 28 (6) (2018): 856-941 (arXiv:1509.07584, doi:10.1017/S0960129517000147)
Auke Booij, Analysis in univalent type theory (2020) [etheses:10411, pdf]
Michael Rathjen, Andrew Swan, Lifschitz Realizability as a Topological Construction. The Journal of Symbolic Logic, Volume 85, Issue 4, December 2020, pp. 1342 - 1375. [doi:10.1017/jsl.2021.1, arXiv:1806.10047]
Francesco Ciraulo, -locales in Formal Topology, Logical Methods in Computer Science, Volume 18, Issue 1 (January 12, 2022) (doi:10.46298/lmcs-18%281%3A7%292022, arXiv:1801.09644)
Andrew Swan (2024) on Category Theory Zulip, Radix expansions in constructive mathematics
Madeleine Birchfield, Andrew Swan (2024) on Category Theory Zulip, LPO and sigma-frame structure on booleans
Andrej Bauer, James Hanson, The Countable Reals (arXiv:2404.01256)
Chris Grossack, Life in Johnstone’s Topological Topos 3 – Bonus Axioms (web)
Henri Lombardi, Assia Mahboubi, Théories géométriques pour l’algèbre des nombres réels sans test de signe ni axiome de choix dépendant (arXiv:2406.15218)
Last revised on July 27, 2024 at 15:14:57. See the history of this page for a list of all contributions to it.